A, B:Type, L:((A(B + Top)) List), x:A.
(can-apply(p-first(L);x))  (fL.can-apply(f;x)) 

latex

Definitions	Top, left + right, x:AB(x), type List, b, (xL.P(x)), P  Q, x:A. B(x), Type, False, P  Q, P  Q, P & Q, x.A(x), t  T, S  T, suptype(S; T), can-apply(f;x), , x. t(x), Void, x:A.B(x), [], x:A  B(x), p_first_nil{p_first_nil_compseq_tag_def:ObjectId}(x), [car / cdr], as @ bs, s ~ t, P  Q, p-first(L), True, T, , (x  l), if b then t else f fi , {T}
Lemmas	p-first-singleton, p-first-append, l exists append, l exists cons, or functionality wrt iff, p-conditional-to-p-first, p-conditional-domain, all functionality wrt iff, iff functionality wrt iff, l exists nil, top wf, iff wf, l exists wf, assert wf, can-apply wf, false wf